$\forall$$T_{1}$, $T_{2}$:Type, $r_{1}$:($T_{1}$$\rightarrow$$T_{1}$$\rightarrow\mathbb{P}$), $r_{2}$:($T_{2}$$\rightarrow$$T_{2}$$\rightarrow\mathbb{P}$).
\\[0ex]($T_{1}$ = $T_{2}$)
\\[0ex]$\Rightarrow$ ($\forall$$x$, $y$:$T_{1}$. $r_{1}$($x$,$y$) $\Leftarrow\!\Rightarrow$ $r_{2}$($x$,$y$))
\\[0ex]$\Rightarrow$ (WellFnd\{i\}($T_{1}$;$x$,$y$.$r_{1}$($x$,$y$)) $\Leftarrow\!\Rightarrow$ WellFnd\{i\}($T_{2}$;$x$,$y$.$r_{2}$($x$,$y$)))